The present invention relates generally to a method and system for carrying out design verification on hardware circuit designs that include combinational loop logic. More specifically, the present invention is directed to a method that can be used in conjunction with existing model checking systems to verify token ring arbitration schemes without requiring modification to the model checker being used.
Formal verification tools refer to a body of software and hardware used to verify the design of a digital circuit and/or computer related hardware. Verification is typically performed prior to the first hardware article being physically manufactured. Thus, the high cost of redesign that attaches after circuits are built is often avoided.
Mathematical models representative of the hardware article""s functional design are initially developed and written in a language, i.e., Verilog or VHDL, which is suitable to be input to a software verification tool, such as VIS. The model, thus developed, is typically a set of formulas that theoretically represent all of the possible conditions of the article being verified. It is common to think of the possible states of a digital system as represented by a set of zeros and ones. A zero typically represents a non-energized (OFF) state of a given signal, input or output, whereas a one represents an energized (ON) state.
In addition to the mathematical model of the circuit design being verified, the verification tool also requires a set of properties against which the model will be checked. These properties are often provided in a form of temporal logic that describes the desired state of the design at different points in time.
Once both the model of the design itself and the properties against which the design will be checked are input to the verification system, an output is provided from the verification system indicating whether or not the modeled design performs the desired functions appropriately given the constraints supplied. If the model checked violates one or more of the properties provided, the system then indicates which particular properties have been violated so appropriate modifications can be made to the model, which in turn may lead to modifications to the circuit design of the hardware article.
Typically, a circuit design can be modeled in state machine format which comprises the set of all possible states that a particular design can occupy at any given time. Once all of the possible states are known, it is determined how the design would get into any particular state, i.e. what inputs are necessary and what prior conditions must be satisfied. This task is not usually particularly difficult for most circuit designs that include flip-flops. Since each change of condition of a flip-flop is considered a change of state, making the development and verification of models for such circuits a relatively straight-forward endeavor. However, when the design being verified contains a combinational loop, wherein no flip-flops exist, the task becomes extremely difficult, if not impossible. In a state-machine that represents a combinational loop, the state of the design at any given time would depend on itself. Conventional model checkers cannot handle this situation because, for example, VIS attempts to express all signals formally before model checking can begin. Since there are no flip-flops between the input and the output of the circuit, the output becomes a combinational function of the input. As a result, a circularity problem arises and the model cannot be verified since no known model checking system can handle this condition. In other words, if a particular circuit design comprises logic formed in a loop topology, with no flip-flops within the loop, the result, or state, of the circuit at any given time will depend directly on its present state; thus causing a circularity problem that presently cannot be resolved without modifying the model checker.
In view of the aforementioned problems with the conventional approach to modeling and verifying the circuit design of hardware systems that contain combinational loop logic, the present invention provides a method whereby circuits that include combinational loop logic can be verified without requiring any changes to the model checker being used.
In one aspect of the invention, a model is provided representing the design of an architecture that employs combinational loop logic. The model might comprise various finite state machines interconnected to one another. A flip-flop is added to break the combinational loop and each of the state machines is modified by providing a twin-state in the state machine corresponding to each original state, effectively doubling the total number of states within each state machine.
More specifically, in accordance with the first aspect of the invention, the steps of determining the location of a combinational loop within a design; providing a model of the design including the combinational loop wherein the model comprises one or more finite state machines, each finite state machine comprising at least one original state; inserting at least one flip-flop within the model, and; providing a twin-state for each original state within each of said finite state machines wherein each twin-state is identical to its respective original state are performed.
As the state machine model is prompted by the verification system to progress through its successive states, the state machine jumps from an original state to the original state""s respective twin-state and then on to the next original state and then on to that original state""s twin-state and so on until the state machine cannot continue given the present inputs. Thus, the combinational loop is modified by placing a flip-flop within the loop and then each finite state machine existing on the loop is modified by adding a second identical state for each original single state.
In a second aspect of the invention the technique described above with respect to the first aspect of the invention is applied to a token ring, or round robin, arbitration scheme of a two level arbitration architecture. Due to typical network communication constraints, a token ring arbitration decision, i.e., which one of a plurality of clients with access to the network will be granted immediate rights to communicate on the bus, must be made within a single cycle of the bus. Thus, according to this aspect of the invention, a combinational loop exists in some implementations of a token ring arbitration scheme. The above mentioned technique is then applied in order to model the design and then apply the resultant model to an existing model checking system. In accordance with the technique discussed above, initially a flip-flop is added to the combinational loop and then each state within the individual state machine models of the token-ring arbitration scheme is provided with a twin state.
More specifically, in accordance with the second aspect of the invention, the steps of developing a finite state machine model for each client on a ring, wherein each finite state machine model comprises at least one original state; inserting a flip-flop model between two of the clients, and; adding a twin-state for each original state within each of the finite state machine models, wherein each twin-state is identical to its respective original state are performed.